$\forall$$T$:(Id$\rightarrow$Type), ${\it tab}$:secret{-}table($T$). ($\uparrow$isl(next(${\it tab}$))) $\Rightarrow$ (ptr(${\it tab}$) $\in$ \{0..$\parallel$${\it tab}$$\parallel$ $^{-}$\})